(set-logic QF_BV)
(declare-fun x () (_ BitVec 1))
(declare-fun y () (_ BitVec 1))
(declare-fun z () Bool)
(assert 
(let ((e26 (= ((_ zero_extend 20) x) (_ bv0 21)))) 
(let ((e35 (= x (_ bv0 1)))) 
(let ((e39 (= (_ bv0 1) y))) 
(let ((e40 (= (_ bv0 1) y))) 
(let ((e55 (= x (_ bv0 1)))) 
(let ((e70 (= true e39))) 
(let ((e71 e55)) 
(let ((e80 (=> e70 false))) 
(let ((e86 (ite e26 e71 z))) 
(let ((e88 (xor e35 false))) 
(let ((e92 (not e86))) 
(let ((e93 (= e92 e40))) 
(let ((e95 (ite e93 false e88))) 
(let ((e101 e95)) 
(let ((e102 (=> e80 false))) 
(let ((e105 e101)) 
(let ((e107 (= false e102))) 
(let ((e109 (=> e105 false))) 
(let ((e115 e107)) 
(let ((e116 (not e115))) 
(let ((e117 (and e116 e109))) e117))))))))))))))))))))))
(check-sat)

